Concurrent programs, also known as multithreaded programs, are found in a wide array of products and services, from software device management to distributed scientific computing. However, the fundamental nature of these programs, the fact that they contain multiple concurrently-executing threads, can cause inter-thread conflicts which can create errors or hanging conditions upon execution. These errors can be particularly difficult to discover when programming because oftentimes more than one asynchronously-running thread is run on a single processor. The instructions of the threads are interleaved, giving rise to a potentially large number of different executions. Because of this, an important, and difficult, part of the debugging and analysis of a concurrent program involves finding potential conflicts between threads.
One of these conflicts is known as a data race. Generally, a data race is a condition where there exists an execution of two or more threads such that the executing computer can arrive at a state for which a) there are two threads which can execute, b) both of these threads access a common variable, and c) at least one of the accesses is a write access.
FIGS. 1a, 1b, 2a, and 2b illustrate two types of data race conditions which can lead to unpredictable results. Avoiding these unpredictable results is the goal of the program analysis discussed below. FIGS. 1a and 1b illustrate one type of data race, that of conflicting read and write instructions from two different threads. In both Figures, there are two concurrently-executing threads which access a common variable, referred to here as “a,” which starts with value 0. The Figures illustrate two different executions of the instructions of Threads 1 and 2. A data race occurs in this example when a computer executing these threads reaches a state at which either of the two executions illustrated could execute. Other than the differing orders, described below, the variable accesses in the Figures are the same
In FIG. 1a, Thread 1, which contains the assignment instruction “q=a,” reads the value of a as 0 and then assigns that value to the variable q. After this point in time, Thread 2 then executes the instruction “a=1” which assigns the value 1 to a. Thus, at the end of the execution of FIG. 1a, a has the value 1 and q has the value 0. In contrast, FIG. 1b illustrates a different execution in which Thread 2 writes to variable a before Thread 1 reads from it. In this case, because a is assigned a value by Thread 2 before Thread 1 is able to read a, q ends up with the value 1. Thus, the two executions illustrated in FIGS. 1a and 1b give two different results for q.
FIGS. 2a and 2b illustrate another type of data race, that of conflicting write instructions. As in FIGS. 1a and 1b, FIGS. 2a and 2b illustrate different executions of instructions from two concurrently-executing threads. In FIG. 2a, Thread 1 executes the instruction “a=0” before Thread 2 executes “a=1,” which results in a having the final value of 1. In contrast, FIG. 2b illustrates the two write commands executing in a differing order, giving α a final value of 0.
The illustrated examples of FIGS. 1a, 1b, 2a, and 2b demonstrate that executions of concurrently-executing threads can cause different values to be placed in certain variables, which can cause a program to behave unpredictably or to fail to execute. Oftentimes, these errors are solved by forcing the competing threads to execute synchronously, which means forcing the threads to operate under a common timing or locking mechanism. The use of synchronous threads allows a programmer to decide ahead of time that certain instructions cannot interfere with each other and to make allowances for that by modifying the programming. However, in order to utilize synchronicity, data races such as those illustrated in FIGS. 1a-1d must be located.
Because data races are so timing-dependent, and may occur under only certain conditions, searching for them in a program can be a difficult, time-consuming process. Data race detection techniques are described with reference to their soundness and preciseness. As used in this application, techniques and systems which are sound are do not fail to miss data races for executions which the techniques investigate. By contrast, the term precise, as used in this application, denotes those techniques which do not generate false positives. That is, techniques that are not precise may report false errors by identifying data races from interleavings of instructions that cannot or will not happen. A precise technique, however, will only report a data race when once truly exists. This means that a data race detection technique that is sound and precise will indicate a data race in a program if, and only if, a data race exists for some execution of the program. What is needed is a sound system for precisely detecting data races in concurrent programs.